\begin{tabbing}
retrace(${\it es}$; $Q$; $X$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$, ${\it e'}$:E. ($Q$($e$,${\it e'}$)) $\Rightarrow$ (($\uparrow$($e$ $\in_{b}$ $X$)) \& ($\uparrow$(${\it e'}$ $\in_{b}$ $X$))))\+
\\[0ex]\& ($\forall$$e$, ${\it e'}$:E($X$). ($Q$($e$,${\it e'}$)) $\vee$ ($e$ = ${\it e'}$) $\vee$ ($Q$(${\it e'}$,$e$)))
\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]$\exists$\=$L$:E List\+
\\[0ex](($\forall$$e$:E. ($e$ $\in$ $L$) $\Leftarrow\!\Rightarrow$ ($Q$($e$,${\it e'}$))) \& ($\forall$$e_{1}$, $e_{2}$:E. $e_{1}$ before $e_{2}$ $\in$ $L$ $\Rightarrow$ ($Q$($e_{1}$,$e_{2}$)))))
\-\-\-
\end{tabbing}